Search for: All records

Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further, reasoning at the level of models instead of program constructs creates a verification gap that loses the benefits of modularity and composition enjoyed by structural program logics such as Hoare Logic. To address this verification gap, and the lack of compositional proof techniques for temporal specifications, we propose Ticl, a new structural temporal logic. Using Ticl, we encode complex (co-)inductive proof techniques as structural lemmas and focus our reasoning on variants and invariants. We show that it is possible to perform compositional proofs of general temporal properties in a proof assistant, while working at a high level of abstraction. We demonstrate the benefits of Ticl by giving mechanized proofs of safety and liveness properties for programs with scheduling, concurrent shared memory, and distributed consensus, demonstrating a low proof-to-code ratio. 

This paper introduces Otti, a general-purpose com- piler for (zk)SNARKs that provides support for numerical op- timization problems. Otti produces efficient arithmetizations of programs that contain optimization problems including linear programming (LP), semi-definite programming (SDP), and a broad class of stochastic gradient descent (SGD) instances. Numerical optimization is a fundamental algorithmic building block: applications include scheduling and resource allocation tasks, approximations to NP-hard problems, and training of neural networks. Otti takes as input arbitrary programs written in a subset of C that contain optimization problems specified via an easy-to-use API. Otti then automatically produces rank-1 constraint satisfiability (R1CS) instances that express a succinct transformation of those programs. Correct execution of the transformed program implies the optimality of the solution to the original optimization problem. Our evaluation on real benchmarks shows that Otti, instantiated with the Spartan proof system, can prove the optimality of solutions in zero-knowledge in as little as 100 ms—over 4 orders of magnitude faster than existing approaches. 

Anthropogenic and natural emissions contribute to enhanced concentrations of aerosols in the Arctic winter and early spring, with most attention being paid to anthropogenic aerosols that contribute to so-called Arctic haze. Less-well-studied wintertime sea-spray aerosols (SSAs) under Arctic haze conditions are the focus of this study, since they can make an important contribution to wintertime Arctic aerosol abundances. Analysis of field campaign data shows evidence for enhanced local sources of SSAs, including marine organics at Utqiaġvik (formerly known as Barrow) in northern Alaska, United States, during winter 2014. Models tend to underestimate sub-micron SSAs and overestimate super-micron SSAs in the Arctic during winter, including the base version of the Weather Research Forecast coupled with Chemistry (WRF-Chem) model used here, which includes a widely used SSA source function based on Gong et al. (1997). Quasi-hemispheric simulations for winter 2014 including updated wind speed and sea-surface temperature (SST) SSA emission dependencies and sources of marine sea-salt organics and sea-salt sulfate lead to significantly improved model performance compared to observations at remote Arctic sites, notably for coarse-mode sodium and chloride, which are reduced. The improved model also simulates more realistic contributions of SSAs to inorganic aerosols at different sites, ranging from 20 %–93 % in the observations. Two-thirds of the improved model performance is from the inclusion of the dependence on SSTs. The simulation of nitrate aerosols is also improved due to less heterogeneous uptake of nitric acid on SSAs in the coarse mode and related increases in fine-mode nitrate. This highlights the importance of interactions between natural SSAs and inorganic anthropogenic aerosols that contribute to Arctic haze. Simulation of organic aerosols and the fraction of sea-salt sulfate are also improved compared to observations. However, the model underestimates episodes with elevated observed concentrations of SSA components and sub-micron non-sea-salt sulfate at some Arctic sites, notably at Utqiaġvik. Possible reasons are explored in higher-resolution runs over northern Alaska for periods corresponding to the Utqiaġvik field campaign in January and February 2014. The addition of a local source of sea-salt marine organics, based on the campaign data, increases modelled organic aerosols over northern Alaska. However, comparison with previous available data suggests that local natural sources from open leads, as well as local anthropogenic sources, are underestimated in the model. Missing local anthropogenic sources may also explain the low modelled (sub-micron) non-sea-salt sulfate at Utqiaġvik. The introduction of a higher wind speed dependence for sub-micron SSA emissions, also based on Arctic data, reduces biases in modelled sub-micron SSAs, while sea-ice fractions, including open leads, are shown to be an important factor controlling modelled super-micron, rather than sub-micron, SSAs over the north coast of Alaska. The regional results presented here show that modelled SSAs are more sensitive to wind speed dependence but that realistic modelling of sea-ice distributions is needed for the simulation of local SSAs, including marine organics. This study supports findings from the Utqiaġvik field campaign that open leads are the primary source of fresh and aged SSAs, including marine organic aerosols, during wintertime at Utqiaġvik; these findings do not suggest an influence from blowing snow and frost flowers. To improve model simulations of Arctic wintertime aerosols, new field data on processes that influence wintertime SSA production, in particular for fine-mode aerosols, are needed as is improved understanding about possible local anthropogenic sources.